perm filename CIRCUM.XGP[F79,JMC] blob sn#492884 filedate 1980-01-09 generic text, type T, neo UTF8
/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30/FONT#11=ZERO30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓α␈↓ α)ADDENDUM: CIRCUMSCRIPTION AND OTHER NON-MONOTONIC FORMALISMS

␈↓ α∧␈↓␈↓ αTCircumscription␈α⊃and␈α⊃the␈α⊂non-monotonic␈α⊃reasoning␈α⊃formalisms␈α⊂of␈α⊃McDermott␈α⊃and␈α⊂Doyle
␈↓ α∧␈↓(1980)␈α∂and␈α∂Reiter␈α⊂(1980)␈α∂differ␈α∂along␈α∂two␈α⊂dimensions.␈α∂ First,␈α∂circumscription␈α∂is␈α⊂concerned␈α∂with
␈↓ α∧␈↓minimal␈αmodels,␈αand␈αthey␈αare␈αconcerned␈αwith␈αarbitrary␈αmodels.␈α It␈αappears␈αthat␈αthese␈αapproaches
␈↓ α∧␈↓solve␈α∂somewhat␈α∂different␈α⊂though␈α∂overlapping␈α∂classes␈α⊂of␈α∂problems,␈α∂and␈α⊂each␈α∂has␈α∂its␈α⊂uses.␈α∂ The
␈↓ α∧␈↓other␈αdifference␈αis␈αthat␈αthe␈αreasoning␈αof␈αboth␈αother␈αformalisms␈αinvolves␈αmodels␈αdirectly,␈αwhile␈αthe
␈↓ α∧␈↓syntactic␈α⊂formulation␈α⊂of␈α⊂circumscription␈α⊂uses␈α⊂axiom␈α⊂schemata.␈α⊂ Consequently,␈α⊂their␈α⊂systems␈α∂are
␈↓ α∧␈↓incompletely formal unless the metamathematics is also formalized.  and this hasn't yet been done.

␈↓ α∧␈↓␈↓ αTHowever,␈α∞schemata␈α
are␈α∞applicable␈α∞to␈α
other␈α∞formalisms␈α
than␈α∞circumscription.␈α∞ Suppose,␈α
for
␈↓ α∧␈↓example,␈α∞that␈α∞we␈α∞have␈α∞some␈α∞axioms␈α∞about␈α∞trains␈α
and␈α∞their␈α∞presence␈α∞on␈α∞tracks,␈α∞and␈α∞we␈α∞wish␈α
to
␈↓ α∧␈↓express␈αthe␈αfact␈α
that␈αif␈αa␈αtrain␈α
may␈αbe␈αpresent,␈αit␈α
is␈αunsafe␈αto␈αcross␈α
the␈αtracks.␈α In␈αthe␈α
McDermott-
␈↓ α∧␈↓Doyle formalism, this might be expressed

␈↓ α∧␈↓1)␈↓ αt ␈↓↓M on(train,tracks) ⊃ ¬safe-to-cross(tracks)␈↓,

␈↓ α∧␈↓where␈α∞the␈α
properties␈α∞of␈α
the␈α∞predicate␈α
␈↓↓on␈↓␈α∞are␈α∞supposed␈α
expressed␈α∞in␈α
a␈α∞formula␈α
that␈α∞we␈α∞may␈α
call
␈↓ α∧␈↓␈↓↓Axiom(on)␈↓.␈α The␈α␈↓↓M␈↓␈αin␈α
(1)␈αstands␈αfor␈α"is␈α
possible".␈α We␈αpropose␈αto␈α
replace␈α(1)␈αand␈α␈↓↓Axiom(on)␈↓␈αby␈α
the
␈↓ α∧␈↓schema

␈↓ α∧␈↓2)␈↓ αt ␈↓↓Axiom(␈↓	F␈↓↓) ∧ ␈↓	F␈↓↓(train,tracks) ⊃ ¬safe-to-cross(tracks)␈↓,

␈↓ α∧␈↓where␈α
␈↓	F␈↓␈α∞is␈α
a␈α
predicate␈α∞parameter␈α
that␈α∞can␈α
be␈α
replaced␈α∞by␈α
any␈α
predicate␈α∞expression␈α
that␈α∞can␈α
be
␈↓ α∧␈↓written␈α∂in␈α∂the␈α∂language␈α∂being␈α∂used.␈α∂ If␈α∂we␈α∂can␈α⊂find␈α∂a␈α∂␈↓	F␈↓␈α∂that␈α∂makes␈α∂the␈α∂left␈α∂hand␈α∂side␈α⊂of␈α∂(2)
␈↓ α∧␈↓provable,␈αthen␈α
we␈αcan␈α
be␈αsure␈α
that␈α␈↓↓Axiom(on)␈↓␈α
together␈αwith␈α
␈↓↓on(train,tracks)␈↓␈αhas␈α
a␈αmodel␈α
assuming
␈↓ α∧␈↓that␈α∀␈↓↓Axiom(on)␈↓␈α∀is␈α∀consistent.␈α∪ Therefore,␈α∀the␈α∀schema␈α∀(2)␈α∪is␈α∀essentially␈α∀a␈α∀consequence␈α∀of␈α∪the
␈↓ α∧␈↓McDermott-Doyle␈α
formula␈α∞(1).␈α
 The␈α∞converse␈α
isn't␈α∞true.␈α
 A␈α∞predicate␈α
symbol␈α∞may␈α
have␈α∞a␈α
model
␈↓ α∧␈↓without␈αthere␈αbeing␈αan␈αexplicit␈αformula␈αrealizing␈αit.␈α I␈αbelieve,␈αhowever,␈αthat␈αthe␈αschema␈αis␈αusable
␈↓ α∧␈↓in␈α
all␈α
cases␈αwhere␈α
the␈α
McDermott-Doyle␈α
or␈αReiter␈α
formalisms␈α
can␈αbe␈α
practically␈α
applied,␈α
and,␈αin
␈↓ α∧␈↓particular, to all the examples in their papers.

␈↓ α∧␈↓␈↓ αT(If␈α⊂one␈α⊂wants␈α⊃a␈α⊂counter-example␈α⊂to␈α⊂the␈α⊃usability␈α⊂of␈α⊂the␈α⊂schema,␈α⊃one␈α⊂might␈α⊂look␈α⊃at␈α⊂the
␈↓ α∧␈↓membership␈α
relation␈αof␈α
set␈αtheory␈α
with␈αG␈↓:␈↓odel-Bernays␈α
set␈α
theory␈αas␈α
the␈αaxiom.␈α
 Instantiating␈α␈↓	F␈↓␈α
in
␈↓ α∧␈↓this␈α
case␈α
would␈α
amount␈α
to␈α
giving␈α
an␈α
internal␈α
model␈α
of␈α
set␈α
theory,␈α
and␈α
this␈α
is␈α
possible␈α
only␈α
in␈α
a
␈↓ α∧␈↓stronger theory).

␈↓ α∧␈↓␈↓ αTIt␈α
appears␈α
that␈α
such␈α
use␈α
of␈α
schemata␈α∞amounts␈α
to␈α
importing␈α
part␈α
of␈α
the␈α
model␈α
theory␈α∞of␈α
a
␈↓ α∧␈↓subject␈αinto␈αthe␈αtheory␈αitself.␈α It␈αlooks␈α
useful␈αand␈αeven␈αessential␈αfor␈αcommon␈αsense␈α
reasoning,␈αbut
␈↓ α∧␈↓its logical properties are not obvious.

␈↓ α∧␈↓␈↓ αTWe can also go frankly to second order logic and write

␈↓ α∧␈↓3)␈↓ αt ␈↓↓∃␈↓	F␈↓↓.(Axiom(␈↓	F␈↓↓) ∧ on(train,tracks) ⊃ ¬safe-to-cross(tracks))␈↓.

␈↓ α∧␈↓Second␈α
order␈α
reasoning,␈α
which␈α
might␈α
be␈α
in␈αset␈α
theory␈α
or␈α
a␈α
formalism␈α
admitting␈α
concepts␈αas␈α
objects
␈↓ α∧␈↓rather␈α∞than␈α∞in␈α
second␈α∞order␈α∞logic,␈α
seems␈α∞to␈α∞have␈α
the␈α∞advantage␈α∞that␈α
some␈α∞of␈α∞the␈α∞predicate␈α
and
␈↓ α∧␈↓function␈α
symbols␈α
may␈αbe␈α
left␈α
fixed␈α
and␈αothers␈α
imitated␈α
by␈α
predicate␈αparameters.␈α
 This␈α
allows␈αus␈α
to
␈↓ α∧␈↓say␈α∂something␈α∞like,␈α∂"For␈α∞any␈α∂interpretation␈α∂of␈α∞␈↓↓P␈↓␈α∂and␈α∞␈↓↓Q␈↓␈α∂satisfying␈α∂the␈α∞axiom␈α∂␈↓↓A,␈↓␈α∞if␈α∂there␈α∂is␈α∞an
␈↓ α∧␈↓␈↓ u2


␈↓ α∧␈↓interpretation␈α
in␈α
which␈α
␈↓↓R␈↓␈α∞and␈α
␈↓↓S␈↓␈α
satisfy␈α
the␈α∞additional␈α
axiom␈α
␈↓↓A',␈↓␈α
then␈α∞it␈α
is␈α
unsafe␈α
to␈α∞cross␈α
the
␈↓ α∧␈↓tracks".␈α
 This␈α
maybe␈α
needed␈α
to␈α
express␈α
common␈α
sense␈α
non-monotonic␈α
reasoning␈α
and␈α
it␈αseems␈α
more
␈↓ α∧␈↓powerful than any of the above-mentioned non-monotonic formalisms including circumscription.

␈↓ α∧␈↓␈↓ αTThe␈α∞train␈α∞example␈α
is␈α∞a␈α∞non-normal␈α
default␈α∞in␈α∞Reiter's␈α
sense,␈α∞because␈α∞we␈α∞cannot␈α
conclude
␈↓ α∧␈↓that␈αthe␈αtrain␈α
is␈αon␈αthe␈αtracks␈α
in␈αthe␈αabsence␈α
of␈αevidence␈αto␈αthe␈α
contrary.␈α Indeed,␈αsuppose␈αthat␈α
we
␈↓ α∧␈↓want␈αto␈αwait␈αfor␈αand␈αcatch␈αa␈αtrain␈αat␈αa␈α
station␈αacross␈αthe␈αtracks.␈α If␈αthere␈αmight␈αbe␈αa␈αtrain␈α
coming
␈↓ α∧␈↓we␈αwill␈α
take␈αa␈α
bridge␈αrather␈αthan␈α
a␈αshortcut␈α
across␈αthe␈α
tracks,␈αbut␈αwe␈α
don't␈αwant␈α
to␈αjump␈α
to␈αthe
␈↓ α∧␈↓conclusion␈αthat␈αthere␈αis␈αa␈αtrain,␈αbecause␈αthen␈αwe␈αwould␈αthink␈αwe␈αwere␈αtoo␈αlate␈αand␈αgive␈αup␈αtrying
␈↓ α∧␈↓to catch it.  The statement can be reformulated as a normal default by writing

␈↓ α∧␈↓4)␈↓ αt ␈↓↓M ¬safe-to-cross(tracks) ⊃ ¬safe-to-cross(tracks)␈↓,

␈↓ α∧␈↓but␈αthis␈αis␈αunlikely␈αto␈αbe␈αequivalent␈αin␈αall␈αcases␈αand␈αthe␈αnon-normal␈αexpression␈αseems␈αto␈αexpress
␈↓ α∧␈↓better the common sense facts.

␈↓ α∧␈↓␈↓ αTLike␈α~normal␈α→defaults,␈α~circumscription␈α~doesn't␈α→deal␈α~with␈α→possibility␈α~directly,␈α~and␈α→a
␈↓ α∧␈↓circumscriptive␈αtreatment␈αof␈αthe␈αtrain␈αproblem␈αwould␈αinvolve␈αcircumscribing␈α␈↓↓safe-to-cross(tracks)␈↓
␈↓ α∧␈↓in the set of axioms.  It therefore might not be completely satisfactory.



␈↓ α∧␈↓Addendum to References:

␈↓ α∧␈↓␈↓αMcDermott,␈α∂Drew␈α∞and␈α∂Jon␈α∞Doyle␈α∂(1980):␈α∞"Non-Monotonic␈α∂Logic␈α∞I",␈α∂␈↓↓Artificial␈α∂Intelligence␈↓,␈α∞this
␈↓ α∧␈↓issue.